Prior art verification of protocols used in concurrent systems required a model, such as a finite state machine or an extended finite state machine, to be developed for each communicating element in the concurrent system. The verification of the protocol between the various communicating elements was then performed on the model. However, verification could not be performed using the actual code, for example C code or C++ code, which implemented the element and described entirely its behavior when the element was actually operating. This is disadvantageous because a) it is time consuming to develop the model and b) the verification is only as good as the accuracy of the model.